Nuprl Lemma : comb_for_hd_wf_listp
4,23
postcript
pdf
(
A
,
l
,
z
. hd(
l
))
A
:Type
A
List
True
A
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
A
List
,
True
,
T
Lemmas
hd
wf
listp
,
squash
wf
,
true
wf
,
listp
wf
origin
A,l,z. hd(l)) 
A:Type
A List
TrueA A,l,z. hd(l)) A:TypeA ListTrueA T
x:A. B(x)T